Skip to content

[Merged by Bors] - chore: avoid superfluous use of push_neg with contrapose, by_contra o…#37937

Closed
grunweg wants to merge 2 commits intoleanprover-community:masterfrom
grunweg:less-neg
Closed

[Merged by Bors] - chore: avoid superfluous use of push_neg with contrapose, by_contra o…#37937
grunweg wants to merge 2 commits intoleanprover-community:masterfrom
grunweg:less-neg

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Apr 11, 2026

…r by_cases

Found by the linter in #37907.

Open in Gitpod

@grunweg grunweg added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 11, 2026
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Apr 11, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Apr 11, 2026 •
edited
Loading

Benchmark results for f7917f4 against 24bf43f are in. There are no significant changes. @grunweg

  • ✅ build//instructions: -5.9G (-0.00%)

No significant changes detected.

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 11, 2026 •
edited
Loading

PR summary 00dbc4ec64

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@grunweg grunweg mentioned this pull request Apr 11, 2026
Open
5 tasks
@JovanGerb
Copy link
Copy Markdown
Contributor

JovanGerb commented Apr 11, 2026

Great! That's a non-trivial amount of tactics cleaned up :). I guess most of these removals are made possible by #31510. I wonder if a similar change should be made to by_cases, namely that if the hypothesis is already a negation, it doesn't make a double negation.

@github-actions github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 11, 2026
@grunweg grunweg mentioned this pull request Apr 11, 2026
Closed
wwylele
wwylele approved these changes Apr 12, 2026
View reviewed changes
Copy link
Copy Markdown
Collaborator

@wwylele wwylele left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see myself got listed in suggested reviewers, likely because I put code with a lot of contrapose! without thinking. If the new guideline is to only use it when needed, then this looks good!

@JovanGerb
Copy link
Copy Markdown
Contributor

JovanGerb commented Apr 13, 2026

maintainer merge

@JovanGerb
Copy link
Copy Markdown
Contributor

JovanGerb commented Apr 13, 2026

Oh, it seems there is a merge conflict. Does the merge conflict label not work anymore?

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 13, 2026

🚀 Pull request has been placed on the maintainer queue by JovanGerb.

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 13, 2026
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Apr 13, 2026

Indeed - merged master.
CC @bryangingechen in case there's something to investigate about the merge conflict workflow. Maybe it just got stuck in the crossfire of github issues these days.

@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented Apr 14, 2026

As far as I can tell the merge conflict label workflow is still working; sometimes it just may take a while (hours? a day?) before the label gets updated because we have so many open PRs and there are token limits.

bryangingechen
bryangingechen approved these changes Apr 14, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@bryangingechen bryangingechen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
bors r+

@mathlib-triage mathlib-triage Bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 14, 2026
mathlib-bors Bot pushed a commit that referenced this pull request Apr 14, 2026
@grunweg
chore: avoid superfluous use of push_neg with contrapose, by_contra o… (
2b93138 
#37937)

…r by_cases

Found by the linter in #37907.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented Apr 14, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore: avoid superfluous use of push_neg with contrapose, by_contra o… [Merged by Bors] - chore: avoid superfluous use of push_neg with contrapose, by_contra o… Apr 14, 2026
@mathlib-bors mathlib-bors Bot closed this Apr 14, 2026
@grunweg grunweg deleted the less-neg branch April 14, 2026 13:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@bryangingechen bryangingechen bryangingechen approved these changes

+1 more reviewer

@wwylele wwylele wwylele approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@grunweg @leanprover-radar @JovanGerb @bryangingechen @wwylele